es:ES, T, A:Type, l:IdLnk, tg, a:Id, ds:x:Id fp Type, P:(State(ds)AProp), f:(State(ds)AT).
weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)  Prop 

latex

Definitions

x:AB(x), P & Q, A & B, t  T, {T}, P  Q, x:A. B(x), ES, Type, IdLnk, Atom$n, Id, a:A fp B(a), x:AB(x), locl(a), A/x,y. B(x;y), 1of(t), E, s = t, b, sender(e), e@i. P(e), valtype(e), val(e), SQType(T), Knd, Prop, s ~ t, left+right, x.A(x), x. t(x), State(ds), source(l), loc(e), {x:A| B(x) }, Top, IdDeq, f(x)?z, vartype(i;x), state@i, state after e, f(a), A, e  e' , rcv(l,tg), kind(e), P  Q, e c e', x:A. B(x), (state when e), weak-precond-send-p(es;T;A;l;tg;a;ds;P;f)

Lemmas

subtype rel wf, es-valtype wf, locl wf, es-state-when wf, alle-at wf, es-causle wf, es-kind wf, rcv wf, es-le wf, not wf, es-state-after wf, subtype rel dep function, subtype rel self, es-vartype wf, fpf-cap wf, id-deq wf, top wf, es-E wf, es-loc wf, lsrc wf, decl-state wf, fpf wf, Id wf, IdLnk wf, event system wf, Knd wf, Knd sq, es-val wf, es-sender wf, es-kind-rcv